{-# LANGUAGE QuasiQuotes, TypeFamilies, FlexibleInstances,
  MultiParamTypeClasses, GADTs, PatternGuards, ViewPatterns,
  StandaloneDeriving, FlexibleContexts, UndecidableInstances, TypeOperators,
  TemplateHaskell, ScopedTypeVariables #-}

{-# OPTIONS_GHC -fcontext-stack=200 #-}

{- |

Module      :  Examples.TermTest
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

A denotational semantics for the simple-typed lambda calculus via
"Data.Yoko.Cata".

-}
module Examples.TermTest where

import Examples.TermBase
import qualified Examples.TermGeneric as G

import Data.Yoko.Cata
import Data.Yoko

import Examples.Eq


-- | Since our family of abstract data types don't correspond to the
-- object-language types, we need a tagged universal value space.
data Val = VBool Bool | VInt Int | VFun (Val -> Val)
instance Show Val where
  show (VBool b) = show b; show (VInt i) = show i; show (VFun _) = "<fun>"



eLam (G.Lam _ t) e = VFun $ t . (: e)
eVar (G.Var i) = (!! i)
eApp (G.App t1 t2) e
  | VFun f <- t1 e = f (t2 e)
  | otherwise = error "failed projection in reduce[App]"
eLet (G.Let ds t) = foldr cons t ds where cons (_, s) t e = t (s e : e)

eDecl (G.Decl ty t) = (ty, t)


-- | The semantic domain of the reduction.
type Sem = [Val] -> Val

-- | The recursion mediator for our denotation.
data SemM = SemM
type instance Med SemM Term = Sem
type instance Med SemM Decl = (Type, Sem)

instance AlgebraDT SemM Term where algebraDT = algebraFin
instance AlgebraDC SemM G.Lam where algebraDC = eLam
instance AlgebraDC SemM G.Var where algebraDC = eVar
instance AlgebraDC SemM G.App where algebraDC = eApp
instance AlgebraDC SemM G.Let where algebraDC = eLet

instance AlgebraDT SemM Decl where algebraDT = eDecl . uniqueRMN

-- | 'eval' will work for any family of mutually recursive types that all have
-- @'AlgebraDT' SemM@ instances.
eval x = ($ x) $ sibCata $ algebras [qP|SemM|]

-- lots of variants on 'eval'
eval_     x = ($ x) $ sibCataTo [qP|SemM|] $ NT $ \td -> case td of
  G.Term__ -> algebraDT
  G.Decl__ -> algebraDT
eval'     x = ($ x) $ cata $ (firstNT toFin $ algebraDT .|. algebraDT :: SiblingAlgs Term SemM)
eval''    x = ($ x) $ sibCataTo [qP|SemM|] $ firstNT toFin $ algebraDT  .|. algebraDT
eval'''   x = ($ x) $ cata $ (firstNT toFin $ algebraFin .|. algebraDT :: SiblingAlgs Term SemM)
eval''''  x = ($ x) $ sibCataTo [qP|SemM|] $ firstNT toFin $ algebraFin .|. algebraDT
eval''''' x = ($ x) $ sibCataTo [qP|SemM|] $ firstNT toFin $ algebraDT .|. (eDecl . uniqueRMN')

instance AlgebraDC SemM G.Decl where algebraDC = eDecl
eval'''''' x = ($ x) $ sibCata $ (firstNT toFin $ algebraFin .|. algebraFin :: SiblingAlgs Term SemM)





vSucc = VFun $ \(VInt i) -> VInt $ i + 1


ex0 = eval (Var 0) [VBool True]
ex1 = eval (Let [Decl (TInt `TArrow` TInt) $ Lam TInt $ Var 1 `App` Var 0]
                (Var 0 `App` Var 2)) [vSucc, VInt 9]
ex2' = eval (Decl TInt (Var 0))
ex2 = snd ex2' [VInt 3]


exUse f = f (Let [Decl (TInt `TArrow` TInt) (Var 0 `App` Var 1)] (Var 0)) [vSucc, VInt 9]

--ex1_ = exUse eval_
--ex1' = exUse eval'
--ex1'' = exUse eval''
--ex1''' = exUse eval'''
--ex1'''' = exUse eval''''
--ex1''''' = exUse eval'''''
--ex1'''''' = exUse eval''''''




-------------------------------------------------------------------------------
-- annotating the types
-------------------------------------------------------------------------------
tLam (G.Lam ty t) e = (ty `TArrow` ty', disbanded $ G.Lam ty t') where
  t'@(ty', _) = t (ty : e)
tVar (G.Var i) e = (e !! i, disbanded $ G.Var i)
tApp (G.App t0 t1) e
  | t0'@(TArrow ((== fst t1') -> True) rng, _) <- t0 e =
    (rng, disbanded $ G.App t0' t1')
  | otherwise = error "failed projection in type[App]"
  where t1' = t1 e
tLet :: RMN StaSemM G.Let -> Med StaSemM Term
tLet (G.Let ds t) = post . foldr cons nil ds where
  post x@(G.Let ds (ty, t)) = (ty, disbanded $ (G.Let ds (ty, t) `asTypeOf` x))
  nil e = G.Let [] (t e)
  cons d sofar e = G.Let (d' : ds) t where
    G.Let ds t = sofar (ty : e)
    d'@(ty, _) = d e

tDecl :: RMN StaSemM G.Decl -> Med StaSemM Decl
tDecl (G.Decl _ t) = t

-- | The recursion mediator for type annotation.
data StaSemM = StaSemM
data StaSem_M = StaSem_M
type instance Med StaSemM t = [Type] -> (Type, Disbanded StaSem_M Term)
type instance Med StaSem_M t = (Type, Disbanded StaSem_M Term)

instance AlgebraDT StaSemM Term where algebraDT = algebraFin
instance AlgebraDC StaSemM G.Lam where algebraDC = tLam
instance AlgebraDC StaSemM G.Var where algebraDC = tVar
instance AlgebraDC StaSemM G.App where algebraDC = tApp
instance AlgebraDC StaSemM G.Let where algebraDC = tLet

instance AlgebraDT StaSemM Decl where algebraDT = tDecl . uniqueRMN

-- | 'typeAnno' will work for any family of mutually recursive types that all
-- have @'AlgebraDT' StaSemM@ instances.
typeAnno x = ($ x) $ sibCata $ algebras [qP|StaSemM|]

ex3 = show $ typeAnno (Let [Decl (TInt `TArrow` TInt) $ Lam TInt $ Var 1 `App` Var 0]
                         (Var 0 `App` Var 2)) [TInt `TArrow` TInt, TInt]

-------------------------------------------------------------------------------
-- showing for NP
-------------------------------------------------------------------------------
data ShowU f dc where ShowU :: Show (Unwrap f dc) => ShowU f dc
obvious_membership ''ShowU
newtype Shower f dc = Shower (Unwrap f dc -> String)
showU :: ShowU f dc -> Unwrap f dc -> String; showU ShowU = show

data ShowUF f dc where ShowUF :: Show (f dc) => ShowUF f dc
obvious_membership ''ShowUF
newtype ShowerF f dc = ShowerF (f dc -> String)
showUF :: ShowUF f dc -> f dc -> String; showUF ShowUF = show

instance (u :=> ShowUF u, u :=> ShowU f) => Show (NP u f) where
  show (NP u x) = "(" ++ showUF (weaken u) u ++
                  ", " ++ showU (weakenTo [qP|ShowU f :: *->*|] u) x ++
                  ")"

type Comp = (:.)
gShow :: (DT t, DCs t :=> ShowU (RM IdM :. N)) => t -> String
gShow (disband -> NP u x) = showU (weakenTo [qP|ShowU (Comp (RM IdM) N) :: *->*|] u) x


-------------------------------------------------------------------------------
-- Eq and Show for Type and Term
-------------------------------------------------------------------------------

-- I need to manage the precedences..., but it otherwise mostly works
--instance Show Term where show = gShow
--instance Show Decl where show = gShow

deriving instance Eq Type

instance Eq Term where (==) = gEq
instance Eq Decl where (==) = gEq

deriving instance (Show (Med m Decl), Show (Med m Term)) => Show (RM m (N G.Let))
deriving instance Show (Med m Term) => Show (RM m (N G.Lam))
deriving instance Show (Med m Term) => Show (RM m (N G.Var))
deriving instance Show (Med m Term) => Show (RM m (N G.App))
deriving instance (Show (Med m Decl), Show (Med m Term)) => Show (RM m (N G.Decl))

deriving instance (Eq (Med m Decl), Eq (Med m Term)) => Eq (RM m (N G.Let))
--deriving instance Eq (Med m Term) => Eq (RM m (N G.Lam))
instance Eq (Med m Term) => Eq (RM m (N G.Lam)) where (==) = repEq
deriving instance Eq (Med m Term) => Eq (RM m (N G.Var))
deriving instance Eq (Med m Term) => Eq (RM m (N G.App))
deriving instance (Eq (Med m Decl), Eq (Med m Term)) => Eq (RM m (N G.Decl))

deriving instance Show (DCs Term a)
deriving instance Show (DCs Decl a)
